/**
 * Software Analysis and Verification 
 * @project: Verify Pattern Matching with Guards in Scala
 * @authors: Mirco Dotta and Philippe Suter
 */

   

package ch.epfl.lara.patterns.ast;


/**
 * Match = ident ':' ident {Pattern}
 */
case class Match (selector: (String,String), patterns: List[Pattern]) {
  override def toString = 
    "(" + selector._1 + ": " + selector._2 + ") match {\n  "+
       "case " + patterns.mkString("\n  case ") + 
    "\n}\n"
}

/**
 * Simplified Scala Grammar for Pattern Matching:
 * Theoretically, we should have all the informations we need to prove some nice
 * properties like disjointness and completeness of pattern matching in Scala.
 *
 * Note: Even if the grammar is simplified we should be able to represent any possible
 * 	 match expression but call functions in the guards.
 *
 * Pattern           ::= KlassPattern | GuardedPattern
 * GuardedPattern    ::= GuardedKlass
 * GuardedKlass      ::= KlassPattern 'if' '(' Guard ')'
 * Guard             ::= Assume(Formula)
 * KlassPattern      ::= AbstractKlass | Klass | Wildcard
 * AbstractKlass     ::= ident '(' ArgsKlassPattern* ')'
 * Klass             ::= ident '(' ArgsKlassPattern* ')'
 * Wildcard          ::= '_' 
 * ArgsKlassPattern* ::= ArgsKlassPattern {',' ArgsKlassPattern*}
 * ArgsKlassPattern  ::= KlassArgument | SimpleArgument
 * KlassArgument     ::= KlassPattern 
 * SimpleArgument    ::= ident  ':' ident 
 * ident             ::= (sequence of character)
 * Formula           ::= All possible formula that cane be created according to FormulaTree
 */

   
sealed abstract class Pattern 

abstract class GuardedPattern extends Pattern

case class GuardedKlass (pattern: KlassPattern, guard: Guard) extends GuardedPattern {
   override def toString = pattern + " if " + guard
 }


import analyze.Constants

abstract class KlassPattern extends Pattern with ArgPattern

case class Klass (klass: String, args: List[ArgPattern]) extends KlassPattern  {
  override def toString = klass + args.mkString("(",",",")")  
}

case class Objekt (name: String) extends KlassPattern {
  override def toString = name 
}

case object Wildcard extends KlassPattern {
  override def toString = "_"
}


abstract class PrimitiveType extends KlassPattern

case class PrimitiveInt(value: Int) extends PrimitiveType


trait ArgPattern 

case class SimpleArgument(ident: String, typeSet: String) extends KlassPattern {
  override def toString = ident + ": " + typeSet
}
    

/**
 * AST for guards. 
 */    
sealed abstract class Guard {
  def getFormula: Formula = this match {
    case Assume(f) => f
  }
}

/** assume(f) */
case class Assume(f: Formula) extends Guard {
  override def toString = "("+f+")"
}
    
